Nuprl Definition : reduce
11,40
postcript
pdf
reduce(
f
;
k
;
as
) == rec-case(
as
) of [] =>
k
|
a
::
as'
=>
.
f
(
a
,reduce(
f
;
k
;
as'
))
(recursive)
latex
Definitions
Y
,
x
.
A
(
x
)
,
rec-case(
a
) of [] =>
s
|
x
::
y
=>
z
.
t
(
x
;
y
;
z
)
,
f
(
a
)
FDL editor aliases
reduce
origin
x.A(x)x.A(x)